(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)


(* L'idea sarà produrre piccoli esempi essenziali che esemplifichino
l'uso delle tattiche. Sarà anche interessante definire 'macro tattiche che
corrispondano alla →E e alla →I di della deduzione naturale. *)

(* 'destruct' -------------------------
                                          Γ
Sia dato Γ ⊢ G nella forma standard   --------- .
                                          G
La tattica 'destruct' applica a G tutte le eguaglianze assunte come
vere perché parte di Γ. Non apre nuovi goal.
 
L'aspetto interessante è che l'applicazione di destruct corrisponde
alla sparizione di goal aperti.
Il motivo è che l'applicazione delle riscritture può portare alla 
comparsa di assunzioni o goal palesemente contraddittori. Ad esempio,
può succedere che compaia:

  costruttore1 = costruttore2

in cui i due costruttori non coincidano. Quella situazione è ignorata.
*)

(* 'lapply' corrispondente alla →E   ----------------------

Supponiamo di aver dimostrato:
  lemma L: A' → B'.

Supponiamo di dover dimostrare:

  Γ ⊢ B           (1)
  
La tattica lapply L produce:

  Γ ⊢ (A'→ B') → B            (2)

Ad esempio, sfruttando le equivalenze in Γ, con le opportune
tattiche, tipo 'destruct', assumiamo di riuscire a trasformare (2) in:

  Γ ⊢ (A → B) → B            (3)

È possibile scaricare A → B con #H, ottenendo:

  Γ, #H:A → B ⊢ B            (4)

L'applicazione di H, ovvero la tattica @H riduce (4) in:

  Γ, #H:A → B ⊢ A            (5)
  
Quindi, la 'macro' corrispondente sembrerebbe essere:

left_arrow hyp = @{#{$hyp} @{$hyp}}
 ma per ora non so bene come definirla, ammesso che lo sia con gli strumenti
 'standard' messi a disposizione e che io conosca.
*)

(* 'lapply' corrispondente alla →I  ----------------------
Supponiamo di avere:

  Γ, #H:A ⊢ B           (1)
  
lapply H scarica H, ovvero produce:

  Γ ⊢ A → B
*)

(* '⋆'  ------------------------------- 
Mi pare d'aver capito, che, applicata ad un goal che sia un tipo induttivo,
equivale alla sequenza di applicazione delle tattiche
#X cases X
anche se non sono sicuro.
*)

(* Espansione della tattica /n/.
Scrivendo /n by _/ la tattica scrive i passi di dimostrazione che segue, in 
analogia con l'espansione delle ipotesi ##. *)

(* Curiosità:
1) provare ad usare [%] con più goal aperti.
2) l'utilizzo della tattica @⊥ che può essere proficuamente utilizzato assieme
alla dimostrazione per assurdo .... non so bene come ....
*)